home *** CD-ROM | disk | FTP | other *** search
| Texinfo Document | 1988-11-16 | 10.0 KB |
open in: 
MacOS 8.1
|
Win98
|
DOS
browse contents |
view JSON data
|
view as text
This file was processed as: Texinfo Document
(document/texInfo).
| Confidence | Program | Detection | Match Type | Support
|
|---|
| 100%
| dexvert
| Texinfo Document (document/texInfo)
| magic
| Supported |
| 1%
| dexvert
| Text File (text/txt)
| fallback
| Supported |
| 100%
| file
| TeX document, ASCII text
| default
| |
| 100%
| checkBytes
| Printable ASCII
| default
| |
| 100%
| perlTextCheck
| Likely Text (Perl)
| default
| |
| 100%
| detectItEasy
| Format: plain text[LF]
| default (weak)
|
|
hex view+--------+-------------------------+-------------------------+--------+--------+
|00000000| 5c 6d 65 73 73 61 67 65 | 7b 4f 4b 2c 20 65 6e 74 |\message|{OK, ent|
|00000010| 65 72 69 6e 67 20 5c 73 | 74 72 69 6e 67 5c 62 61 |ering \s|tring\ba|
|00000020| 74 63 68 6d 6f 64 65 2e | 2e 2e 7d 0a 5c 62 61 74 |tchmode.|..}.\bat|
|00000030| 63 68 6d 6f 64 65 0a 5c | 6f 76 65 72 66 75 6c 6c |chmode.\|overfull|
|00000040| 72 75 6c 65 30 70 74 0a | 5c 69 6e 70 75 74 20 65 |rule0pt.|\input e|
|00000050| 6e 75 6d 65 72 61 74 65 | 0a 5c 64 65 66 5c 56 43 |numerate|.\def\VC|
|00000060| 23 31 23 32 7b 7b 5c 65 | 6e 75 6d 65 72 61 74 65 |#1#2{{\e|numerate|
|00000070| 5c 69 74 65 6d 20 23 31 | 5c 65 6e 64 65 6e 75 6d |\item #1|\endenum|
|00000080| 65 72 61 74 65 5c 70 61 | 72 7d 7b 24 3e 5c 21 5c |erate\pa|r}{$>\!\|
|00000090| 21 3e 24 5c 20 23 32 5c | 70 61 72 7d 7d 0a 25 5c |!>$\ #2\|par}}.%\|
|000000a0| 70 61 72 69 6e 64 65 6e | 74 3d 30 70 74 5c 70 61 |parinden|t=0pt\pa|
|000000b0| 72 73 6b 69 70 3d 30 2e | 35 5c 62 61 73 65 6c 69 |rskip=0.|5\baseli|
|000000c0| 6e 65 73 6b 69 70 0a 5c | 6c 65 74 5c 6d 61 70 73 |neskip.\|let\maps|
|000000d0| 5c 72 69 67 68 74 61 72 | 72 6f 77 0a 5c 64 65 66 |\rightar|row.\def|
|000000e0| 5c 74 69 74 6c 65 7b 41 | 20 47 65 6e 65 72 69 63 |\title{A| Generic|
|000000f0| 20 53 74 61 63 6b 20 50 | 61 63 6b 61 67 65 7d 0a | Stack P|ackage}.|
|00000100| 0a 40 2a 53 74 61 63 6b | 73 2e 0a 54 68 65 20 69 |.@*Stack|s..The i|
|00000110| 64 65 61 20 69 73 20 74 | 6f 20 69 6d 70 6c 65 6d |dea is t|o implem|
|00000120| 65 6e 74 2c 20 61 6e 64 | 20 74 6f 20 70 72 6f 76 |ent, and| to prov|
|00000130| 65 20 70 61 72 74 20 6f | 66 2c 20 61 20 73 69 6d |e part o|f, a sim|
|00000140| 70 6c 65 20 73 74 61 63 | 6b 20 70 61 63 6b 61 67 |ple stac|k packag|
|00000150| 65 2e 0a 57 65 20 77 72 | 69 74 65 20 61 20 4c 61 |e..We wr|ite a La|
|00000160| 72 63 68 20 74 72 61 69 | 74 20 66 6f 72 20 74 68 |rch trai|t for th|
|00000170| 65 20 73 74 61 63 6b 73 | 2c 0a 77 65 20 75 73 65 |e stacks|,.we use|
|00000180| 20 74 65 72 6d 73 20 6f | 66 20 74 68 61 74 20 74 | terms o|f that t|
|00000190| 72 61 69 74 20 74 6f 20 | 73 70 65 63 69 66 79 20 |rait to |specify |
|000001a0| 6f 75 72 20 70 61 63 6b | 61 67 65 2e 0a 20 49 6e |our pack|age.. In|
|000001b0| 20 74 68 65 20 70 61 63 | 6b 61 67 65 20 62 6f 64 | the pac|kage bod|
|000001c0| 79 20 77 65 20 77 72 69 | 74 65 20 64 6f 77 6e 20 |y we wri|te down |
|000001d0| 61 6e 20 65 78 70 6c 69 | 63 69 74 0a 72 65 70 72 |an expli|cit.repr|
|000001e0| 65 73 65 6e 74 61 74 69 | 6f 6e 20 69 6e 76 61 72 |esentati|on invar|
|000001f0| 69 61 6e 74 20 7c 69 6e | 76 61 72 7c 20 61 6e 64 |iant |in|var| and|
|00000200| 20 61 6e 20 65 78 70 6c | 69 63 69 74 20 61 62 73 | an expl|icit abs|
|00000210| 74 72 61 63 74 69 6f 6e | 20 66 75 6e 63 74 69 6f |traction| functio|
|00000220| 6e 0a 7c 61 62 73 74 72 | 61 63 74 69 6f 6e 7c 2c |n.|abstr|action|,|
|00000230| 20 61 6e 64 20 77 65 20 | 75 73 65 20 74 68 65 6d | and we |use them|
|00000240| 20 74 6f 20 70 72 6f 76 | 65 20 74 68 65 20 70 61 | to prov|e the pa|
|00000250| 63 6b 61 67 65 20 5c 60 | 61 20 6c 61 20 48 6f 61 |ckage \`|a la Hoa|
|00000260| 72 65 2e 0a 54 68 65 20 | 70 61 63 6b 61 67 65 20 |re..The |package |
|00000270| 73 70 65 63 69 66 69 63 | 61 74 69 6f 6e 20 72 65 |specific|ation re|
|00000280| 66 65 72 73 20 6f 6e 6c | 79 20 74 6f 20 74 68 65 |fers onl|y to the|
|00000290| 20 61 62 73 74 72 61 63 | 74 20 74 72 61 69 74 2c | abstrac|t trait,|
|000002a0| 0a 61 6e 64 20 6f 75 72 | 20 73 6f 66 74 77 61 72 |.and our| softwar|
|000002b0| 65 20 77 69 6c 6c 20 61 | 75 74 6f 6d 61 74 69 63 |e will a|utomatic|
|000002c0| 61 6c 6c 79 20 70 65 72 | 66 6f 72 6d 20 74 68 65 |ally per|form the|
|000002d0| 20 74 72 61 6e 73 6c 61 | 74 69 6f 6e 20 72 65 71 | transla|tion req|
|000002e0| 75 69 72 65 64 0a 74 6f | 20 69 6e 74 72 6f 64 75 |uired.to| introdu|
|000002f0| 63 65 20 65 78 70 6c 69 | 63 69 74 20 69 6e 76 61 |ce expli|cit inva|
|00000300| 72 69 61 6e 74 73 20 61 | 6e 64 20 61 62 73 74 72 |riants a|nd abstr|
|00000310| 61 63 74 69 6f 6e 20 66 | 75 6e 63 74 69 6f 6e 73 |action f|unctions|
|00000320| 20 69 6e 20 74 68 65 0a | 70 61 63 6b 61 67 65 20 | in the.|package |
|00000330| 62 6f 64 79 2e 0a 0a 40 | 2a 54 68 65 6f 72 79 20 |body...@|*Theory |
|00000340| 6f 66 20 73 74 61 63 6b | 73 2e 0a 57 65 20 75 73 |of stack|s..We us|
|00000350| 65 20 74 68 65 20 66 6f | 6c 6c 6f 77 69 6e 67 20 |e the fo|llowing |
|00000360| 74 68 65 6f 72 79 3a 0a | 25 5c 69 6e 70 75 74 20 |theory:.|%\input |
|00000370| 73 74 61 63 6b 74 72 61 | 69 74 2e 70 72 65 74 74 |stacktra|it.prett|
|00000380| 79 0a 0a 0a 40 2a 53 70 | 65 63 69 66 69 63 61 74 |y...@*Sp|ecificat|
|00000390| 69 6f 6e 2e 0a 57 65 20 | 6e 6f 77 20 75 73 65 20 |ion..We |now use |
|000003a0| 74 68 65 20 7c 53 74 61 | 63 6b 5f 74 68 65 6f 72 |the |Sta|ck_theor|
|000003b0| 79 7c 20 74 72 61 69 74 | 20 74 6f 20 73 70 65 63 |y| trait| to spec|
|000003c0| 69 66 79 20 61 20 70 61 | 63 6b 61 67 65 2e 0a 54 |ify a pa|ckage..T|
|000003d0| 68 65 20 70 68 72 61 73 | 65 20 0a 7c 77 69 74 68 |he phras|e .|with|
|000003e0| 20 74 72 61 69 74 20 53 | 74 61 63 6b 5f 74 68 65 | trait S|tack_the|
|000003f0| 6f 72 79 7c 0a 6d 61 6b | 65 73 20 74 68 65 20 7c |ory|.mak|es the ||
|00000400| 53 74 61 63 6b 5f 74 68 | 65 6f 72 79 7c 20 74 72 |Stack_th|eory| tr|
|00000410| 61 69 74 20 76 69 73 69 | 62 6c 65 20 61 6e 64 0a |ait visi|ble and.|
|00000420| 74 68 65 20 70 68 72 61 | 73 65 0a 7c 62 61 73 65 |the phra|se.|base|
|00000430| 64 20 6f 6e 20 73 74 61 | 63 6b 7c 0a 6d 61 6b 65 |d on sta|ck|.make|
|00000440| 73 20 74 68 65 20 73 6f | 72 74 20 7c 73 74 61 63 |s the so|rt |stac|
|00000450| 6b 7c 20 66 72 6f 6d 20 | 7c 53 74 61 63 6b 5f 74 |k| from ||Stack_t|
|00000460| 68 65 6f 72 79 7c 20 74 | 68 65 20 61 62 73 74 72 |heory| t|he abstr|
|00000470| 61 63 74 20 73 6f 72 74 | 20 7c 73 74 61 63 6b 27 |act sort| |stack'|
|00000480| 41 42 53 54 52 41 43 54 | 7c 2e 20 0a 57 65 20 61 |ABSTRACT||. .We a|
|00000490| 6c 73 6f 20 75 73 65 20 | 74 68 65 20 7c 65 6c 65 |lso use |the |ele|
|000004a0| 6d 65 6e 74 7c 20 73 6f | 72 74 20 74 6f 20 72 65 |ment| so|rt to re|
|000004b0| 70 72 65 73 65 6e 74 20 | 74 68 65 20 70 72 69 76 |present |the priv|
|000004c0| 61 74 65 20 74 79 70 65 | 20 7c 65 6c 65 6d 65 6e |ate type| |elemen|
|000004d0| 74 7c 2e 0a 25 20 41 43 | 4b 21 20 57 68 61 74 20 |t|..% AC|K! What |
|000004e0| 70 72 6f 6f 66 20 6f 62 | 6c 69 67 61 74 69 6f 6e |proof ob|ligation|
|000004f0| 73 20 64 6f 65 73 20 74 | 68 69 73 20 67 69 76 65 |s does t|his give|
|00000500| 3f 0a 0a 49 6e 20 74 68 | 65 20 70 61 63 6b 61 67 |?..In th|e packag|
|00000510| 65 20 7b 5c 69 74 20 73 | 70 65 63 69 66 69 63 61 |e {\it s|pecifica|
|00000520| 74 69 6f 6e 7d 2c 20 61 | 6c 6c 20 74 65 72 6d 73 |tion}, a|ll terms|
|00000530| 20 6f 66 20 74 79 70 65 | 20 7c 73 74 61 63 6b 7c | of type| |stack||
|00000540| 20 61 72 65 0a 73 70 65 | 63 69 66 69 65 64 20 77 | are.spe|cified w|
|00000550| 69 74 68 20 74 65 72 6d | 73 20 6f 66 20 74 79 70 |ith term|s of typ|
|00000560| 65 20 7c 53 74 61 63 6b | 73 5f 74 68 65 6f 72 79 |e |Stack|s_theory|
|00000570| 2e 73 74 61 63 6b 7c 2e | 0a 49 6e 20 74 68 65 20 |.stack|.|.In the |
|00000580| 70 61 63 6b 61 67 65 20 | 7b 5c 69 74 20 62 6f 64 |package |{\it bod|
|00000590| 79 7d 2c 20 77 65 20 77 | 69 6c 6c 20 73 70 65 63 |y}, we w|ill spec|
|000005a0| 69 66 79 20 74 65 72 6d | 73 20 6f 66 20 74 79 70 |ify term|s of typ|
|000005b0| 65 20 7c 73 74 61 63 6b | 7c 20 77 69 74 68 0a 74 |e |stack|| with.t|
|000005c0| 65 72 6d 73 20 6f 66 20 | 61 20 73 6f 72 74 20 63 |erms of |a sort c|
|000005d0| 6f 72 72 65 73 70 6f 6e | 64 69 6e 67 20 74 6f 20 |orrespon|ding to |
|000005e0| 74 68 65 20 70 72 69 76 | 61 74 65 20 74 79 70 65 |the priv|ate type|
|000005f0| 20 6f 66 20 73 74 61 63 | 6b 20 28 69 6e 20 74 68 | of stac|k (in th|
|00000600| 69 73 0a 69 6e 73 74 61 | 6e 63 65 2c 20 61 20 72 |is.insta|nce, a r|
|00000610| 65 63 6f 72 64 20 74 79 | 70 65 29 2e 0a 57 65 20 |ecord ty|pe)..We |
|00000620| 77 69 6c 6c 20 70 72 6f | 76 69 64 65 20 61 6e 20 |will pro|vide an |
|00000630| 61 62 73 74 72 61 63 74 | 69 6f 6e 20 66 75 6e 63 |abstract|ion func|
|00000640| 74 69 6f 6e 20 66 72 6f | 6d 20 74 65 72 6d 73 20 |tion fro|m terms |
|00000650| 6f 66 20 74 68 65 20 72 | 65 63 6f 72 64 20 74 72 |of the r|ecord tr|
|00000660| 61 69 74 0a 74 6f 20 74 | 65 72 6d 73 20 6f 66 20 |ait.to t|erms of |
|00000670| 74 68 65 20 73 74 61 63 | 6b 20 74 72 61 69 74 2c |the stac|k trait,|
|00000680| 20 61 6e 64 20 61 6e 20 | 69 6e 76 61 72 69 61 6e | and an |invarian|
|00000690| 74 20 66 75 6e 63 74 69 | 6f 6e 20 66 72 6f 6d 20 |t functi|on from |
|000006a0| 74 65 72 6d 73 20 6f 66 | 0a 74 68 65 20 72 65 63 |terms of|.the rec|
|000006b0| 6f 72 64 20 74 72 61 69 | 74 20 74 6f 20 7c 62 6f |ord trai|t to |bo|
|000006c0| 6f 6c 65 61 6e 7c 2e 0a | 40 63 40 30 0a 67 65 6e |olean|..|@c@0.gen|
|000006d0| 65 72 69 63 0a 20 20 20 | 20 20 20 20 20 74 79 70 |eric. | typ|
|000006e0| 65 20 65 6c 65 6d 65 6e | 74 20 69 73 20 70 72 69 |e elemen|t is pri|
|000006f0| 76 61 74 65 3b 20 0a 20 | 20 20 20 20 20 20 20 6c |vate; . | l|
|00000700| 65 6e 67 74 68 3a 20 6e | 61 74 75 72 61 6c 20 3a |ength: n|atural :|
|00000710| 3d 20 31 30 30 3b 0a 70 | 61 63 6b 61 67 65 20 73 |= 100;.p|ackage s|
|00000720| 74 61 63 6b 73 20 69 73 | 0a 09 0a 20 20 20 20 20 |tacks is|... |
|00000730| 20 20 20 74 79 70 65 20 | 73 74 61 63 6b 20 69 73 | type |stack is|
|00000740| 20 70 72 69 76 61 74 65 | 3b 0a 40 2f 09 0a 20 20 | private|;.@/.. |
|00000750| 20 20 20 20 20 20 6f 76 | 65 72 66 6c 6f 77 2c 20 | ov|erflow, |
|00000760| 75 6e 64 65 72 66 6c 6f | 77 3a 20 65 78 63 65 70 |underflo|w: excep|
|00000770| 74 69 6f 6e 3b 0a 40 23 | 0a 20 20 20 20 20 20 20 |tion;.@#|. |
|00000780| 20 66 75 6e 63 74 69 6f | 6e 20 65 6d 70 74 79 5f | functio|n empty_|
|00000790| 73 74 61 63 6b 20 72 65 | 74 75 72 6e 20 73 74 61 |stack re|turn sta|
|000007a0| 63 6b 3b 0a 20 20 20 20 | 20 20 20 20 0a 0a 40 23 |ck;. | ..@#|
|000007b0| 0a 20 20 20 20 20 20 20 | 20 66 75 6e 63 74 69 6f |. | functio|
|000007c0| 6e 20 70 75 73 68 69 74 | 28 73 3a 73 74 61 63 6b |n pushit|(s:stack|
|000007d0| 3b 20 65 3a 65 6c 65 6d | 65 6e 74 29 20 72 65 74 |; e:elem|ent) ret|
|000007e0| 75 72 6e 20 73 74 61 63 | 6b 3b 0a 20 20 20 20 20 |urn stac|k;. |
|000007f0| 20 20 20 0a 20 20 20 20 | 20 20 20 20 0a 20 20 20 | . | . |
|00000800| 20 20 20 20 20 0a 20 20 | 20 20 20 20 20 20 0a 40 | . | .@|
|00000810| 23 0a 20 20 20 20 20 20 | 20 20 66 75 6e 63 74 69 |#. | functi|
|00000820| 6f 6e 20 70 6f 70 69 74 | 28 73 3a 73 74 61 63 6b |on popit|(s:stack|
|00000830| 29 20 72 65 74 75 72 6e | 20 73 74 61 63 6b 3b 0a |) return| stack;.|
|00000840| 20 20 20 20 20 20 20 20 | 0a 20 20 20 20 20 20 20 | |. |
|00000850| 20 0a 20 20 20 20 20 20 | 20 20 0a 20 20 20 20 20 | . | . |
|00000860| 20 20 20 0a 40 23 0a 20 | 20 20 20 20 20 20 20 66 | .@#. | f|
|00000870| 75 6e 63 74 69 6f 6e 20 | 74 6f 70 69 74 28 73 3a |unction |topit(s:|
|00000880| 73 74 61 63 6b 29 20 72 | 65 74 75 72 6e 20 65 6c |stack) r|eturn el|
|00000890| 65 6d 65 6e 74 3b 0a 20 | 20 20 20 20 20 20 20 0a |ement;. | .|
|000008a0| 20 20 20 20 20 20 20 20 | 0a 20 20 20 20 20 20 20 | |. |
|000008b0| 20 0a 20 20 20 20 20 20 | 20 20 0a 40 23 0a 20 20 | . | .@#. |
|000008c0| 20 20 66 75 6e 63 74 69 | 6f 6e 20 69 73 45 6d 70 | functi|on isEmp|
|000008d0| 74 79 28 73 3a 73 74 61 | 63 6b 29 20 72 65 74 75 |ty(s:sta|ck) retu|
|000008e0| 72 6e 20 62 6f 6f 6c 65 | 61 6e 3b 0a 09 0a 09 0a |rn boole|an;.....|
|000008f0| 09 0a 0a 70 72 69 76 61 | 74 65 0a 20 20 20 20 73 |...priva|te. s|
|00000900| 75 62 74 79 70 65 20 73 | 74 61 63 6b 5f 72 61 6e |ubtype s|tack_ran|
|00000910| 67 65 20 69 73 20 6e 61 | 74 75 72 61 6c 20 72 61 |ge is na|tural ra|
|00000920| 6e 67 65 20 30 2e 2e 20 | 6c 65 6e 67 74 68 20 2d |nge 0.. |length -|
|00000930| 20 31 3b 0a 20 20 20 20 | 74 79 70 65 20 73 74 61 | 1;. |type sta|
|00000940| 63 6b 5f 61 72 72 61 79 | 20 69 73 20 61 72 72 61 |ck_array| is arra|
|00000950| 79 28 73 74 61 63 6b 5f | 72 61 6e 67 65 29 20 6f |y(stack_|range) o|
|00000960| 66 20 65 6c 65 6d 65 6e | 74 3b 0a 20 20 20 20 74 |f elemen|t;. t|
|00000970| 79 70 65 20 73 74 61 63 | 6b 20 69 73 0a 20 20 20 |ype stac|k is. |
|00000980| 20 72 65 63 6f 72 64 0a | 09 6c 3a 20 6e 61 74 75 | record.|.l: natu|
|00000990| 72 61 6c 3b 09 2d 2d 20 | 6c 65 6e 67 74 68 0a 09 |ral;.-- |length..|
|000009a0| 61 3a 20 73 74 61 63 6b | 5f 61 72 72 61 79 3b 09 |a: stack|_array;.|
|000009b0| 2d 2d 73 74 61 63 6b 0a | 20 20 20 20 65 6e 64 20 |--stack.| end |
|000009c0| 72 65 63 6f 72 64 3b 0a | 0a 65 6e 64 20 73 74 61 |record;.|.end sta|
|000009d0| 63 6b 73 3b 0a 40 2a 49 | 6d 70 6c 65 6d 65 6e 74 |cks;.@*I|mplement|
|000009e0| 61 74 69 6f 6e 2e 0a 57 | 65 20 62 72 65 61 6b 20 |ation..W|e break |
|000009f0| 74 68 65 20 69 6d 70 6c | 65 6d 65 6e 74 61 74 69 |the impl|ementati|
|00000a00| 6f 6e 20 69 6e 74 6f 20 | 70 69 65 63 65 73 20 73 |on into |pieces s|
|00000a10| 6f 20 77 65 20 63 61 6e | 20 64 69 73 63 75 73 73 |o we can| discuss|
|00000a20| 20 74 68 65 6d 20 6f 6e | 65 20 61 74 0a 61 20 74 | them on|e at.a t|
|00000a30| 69 6d 65 2e 0a 0a 57 69 | 74 68 69 6e 20 74 68 65 |ime...Wi|thin the|
|00000a40| 20 68 69 64 64 65 6e 20 | 70 61 72 74 20 6f 66 20 | hidden |part of |
|00000a50| 74 68 65 20 70 61 63 6b | 61 67 65 2c 20 7c 73 74 |the pack|age, |st|
|00000a60| 61 63 6b 7c 20 77 69 6c | 6c 20 73 74 61 6e 64 20 |ack| wil|l stand |
|00000a70| 66 6f 72 20 74 68 65 0a | 63 6f 6e 63 72 65 74 65 |for the.|concrete|
|00000a80| 20 74 79 70 65 20 28 6f | 72 20 73 6f 72 74 29 2c | type (o|r sort),|
|00000a90| 20 7c 73 74 61 63 6b 27 | 43 4f 4e 43 52 45 54 45 | |stack'|CONCRETE|
|00000aa0| 7c 2e 0a 4f 75 74 73 69 | 64 65 2c 20 69 6e 20 74 ||..Outsi|de, in t|
|00000ab0| 68 65 20 73 70 65 63 69 | 66 69 63 61 74 69 6f 6e |he speci|fication|
|00000ac0| 2c 20 7c 73 74 61 63 6b | 7c 20 77 69 6c 6c 20 73 |, |stack|| will s|
|00000ad0| 74 61 6e 64 20 66 6f 72 | 20 74 68 65 20 61 62 73 |tand for| the abs|
|00000ae0| 74 72 61 63 74 0a 74 79 | 70 65 20 28 6f 72 20 73 |tract.ty|pe (or s|
|00000af0| 6f 72 74 29 2c 20 7c 73 | 74 61 63 6b 27 41 42 53 |ort), |s|tack'ABS|
|00000b00| 54 52 41 43 54 7c 2e 0a | 57 65 20 75 73 65 20 74 |TRACT|..|We use t|
|00000b10| 79 70 65 73 20 69 6e 20 | 61 63 74 75 61 6c 20 41 |ypes in |actual A|
|00000b20| 64 61 20 63 6f 64 65 2c | 20 61 6e 64 20 73 6f 72 |da code,| and sor|
|00000b30| 74 73 20 69 6e 20 61 6e | 6e 6f 74 61 74 69 6f 6e |ts in an|notation|
|00000b40| 73 20 61 6e 64 20 76 69 | 72 74 75 61 6c 0a 66 75 |s and vi|rtual.fu|
|00000b50| 6e 63 74 69 6f 6e 73 2e | 0a 0a 40 63 0a 67 65 6e |nctions.|..@c.gen|
|00000b60| 65 72 69 63 0a 20 20 20 | 20 20 20 20 20 74 79 70 |eric. | typ|
|00000b70| 65 20 65 6c 65 6d 65 6e | 74 20 69 73 20 70 72 69 |e elemen|t is pri|
|00000b80| 76 61 74 65 3b 0a 20 20 | 20 20 20 20 20 20 6c 65 |vate;. | le|
|00000b90| 6e 67 74 68 3a 20 6e 61 | 74 75 72 61 6c 20 3a 3d |ngth: na|tural :=|
|00000ba0| 20 31 30 30 3b 0a 70 61 | 63 6b 61 67 65 20 62 6f | 100;.pa|ckage bo|
|00000bb0| 64 79 20 73 74 61 63 6b | 73 20 69 73 0a 40 3c 41 |dy stack|s is.@<A|
|00000bc0| 62 73 74 72 61 63 74 69 | 6f 6e 20 61 6e 64 20 69 |bstracti|on and i|
|00000bd0| 6e 76 61 72 69 61 6e 74 | 73 40 3e 40 3b 0a 40 3c |nvariant|s@>@;.@<|
|00000be0| 49 6d 70 6c 65 6d 65 6e | 74 61 74 69 6f 6e 20 6f |Implemen|tation o|
|00000bf0| 66 20 7c 65 6d 70 74 79 | 5f 73 74 61 63 6b 7c 40 |f |empty|_stack|@|
|00000c00| 3e 40 3b 0a 40 3c 49 6d | 70 6c 65 6d 65 6e 74 61 |>@;.@<Im|plementa|
|00000c10| 74 69 6f 6e 20 6f 66 20 | 7c 70 75 73 68 69 74 7c |tion of ||pushit||
|00000c20| 40 3e 40 3b 0a 40 3c 49 | 6d 70 6c 65 6d 65 6e 74 |@>@;.@<I|mplement|
|00000c30| 61 74 69 6f 6e 20 6f 66 | 20 7c 70 6f 70 69 74 7c |ation of| |popit||
|00000c40| 40 3e 40 3b 0a 40 3c 49 | 6d 70 6c 65 6d 65 6e 74 |@>@;.@<I|mplement|
|00000c50| 61 74 69 6f 6e 20 6f 66 | 20 7c 74 6f 70 69 74 7c |ation of| |topit||
|00000c60| 40 3e 40 3b 0a 40 3c 49 | 6d 70 6c 65 6d 65 6e 74 |@>@;.@<I|mplement|
|00000c70| 61 74 69 6f 6e 20 6f 66 | 20 7c 69 73 45 6d 70 74 |ation of| |isEmpt|
|00000c80| 79 7c 40 3e 40 3b 0a 65 | 6e 64 20 73 74 61 63 6b |y|@>@;.e|nd stack|
|00000c90| 73 3b 0a 40 20 48 65 72 | 65 20 77 65 20 6d 61 6b |s;.@ Her|e we mak|
|00000ca0| 65 20 65 78 70 6c 69 63 | 69 74 20 74 68 65 20 72 |e explic|it the r|
|00000cb0| 65 70 72 65 73 65 6e 74 | 61 74 69 6f 6e 20 69 6e |epresent|ation in|
|00000cc0| 76 61 72 69 61 6e 74 20 | 7c 69 6e 76 61 72 7c 20 |variant ||invar| |
|00000cd0| 61 6e 64 20 74 68 65 0a | 61 62 73 74 72 61 63 74 |and the.|abstract|
|00000ce0| 69 6f 6e 20 66 75 6e 63 | 74 69 6f 6e 20 7c 61 62 |ion func|tion |ab|
|00000cf0| 73 74 72 61 63 74 69 6f | 6e 7c 2e 0a 54 68 65 73 |stractio|n|..Thes|
|00000d00| 65 20 61 72 65 20 76 69 | 72 74 75 61 6c 20 66 75 |e are vi|rtual fu|
|00000d10| 6e 63 74 69 6f 6e 73 2c | 20 61 6e 64 20 74 65 6d |nctions,| and tem|
|00000d20| 70 6c 61 74 65 73 20 66 | 6f 72 20 74 68 65 6d 20 |plates f|or them |
|00000d30| 77 69 6c 6c 20 62 65 20 | 67 65 6e 65 72 61 74 65 |will be |generate|
|00000d40| 64 0a 61 75 74 6f 6d 61 | 74 69 63 61 6c 6c 79 20 |d.automa|tically |
|00000d50| 66 72 6f 6d 20 74 68 65 | 20 70 61 63 6b 61 67 65 |from the| package|
|00000d60| 20 73 70 65 63 69 66 69 | 63 61 74 69 6f 6e 2e 0a | specifi|cation..|
|00000d70| 54 68 65 73 65 20 66 75 | 6e 63 74 69 6f 6e 73 20 |These fu|nctions |
|00000d80| 77 69 6c 6c 20 61 70 70 | 65 61 72 20 69 6e 20 74 |will app|ear in t|
|00000d90| 68 65 20 61 6e 6e 6f 74 | 61 74 69 6f 6e 73 20 66 |he annot|ations f|
|00000da0| 6f 72 20 74 68 65 20 6f | 70 65 72 61 74 69 6f 6e |or the o|peration|
|00000db0| 73 20 6f 66 0a 74 68 65 | 20 70 61 63 6b 61 67 65 |s of.the| package|
|00000dc0| 2c 20 77 68 69 63 68 20 | 77 69 6c 6c 20 61 6c 73 |, which |will als|
|00000dd0| 6f 20 68 61 76 65 20 62 | 65 65 6e 20 74 72 61 6e |o have b|een tran|
|00000de0| 73 6c 61 74 65 64 20 66 | 72 6f 6d 20 74 68 65 20 |slated f|rom the |
|00000df0| 70 61 63 6b 61 67 65 0a | 73 70 65 63 69 66 69 63 |package.|specific|
|00000e00| 61 74 69 6f 6e 2e 0a 0a | 54 68 65 20 69 6e 76 61 |ation...|The inva|
|00000e10| 72 69 61 6e 74 20 72 65 | 71 75 69 72 65 73 20 6f |riant re|quires o|
|00000e20| 6e 6c 79 20 74 68 61 74 | 20 74 68 65 20 6c 65 6e |nly that| the len|
|00000e30| 67 74 68 20 62 65 20 77 | 69 74 68 69 6e 20 73 65 |gth be w|ithin se|
|00000e40| 6e 73 69 62 6c 65 20 62 | 6f 75 6e 64 73 2e 0a 28 |nsible b|ounds..(|
|00000e50| 49 20 68 61 76 65 20 69 | 67 6e 6f 72 65 64 20 74 |I have i|gnored t|
|00000e60| 68 65 20 70 72 6f 62 6c | 65 6d 20 6f 66 20 64 65 |he probl|em of de|
|00000e70| 66 69 6e 65 64 6e 65 73 | 73 20 74 68 72 6f 75 67 |finednes|s throug|
|00000e80| 68 6f 75 74 20 74 68 65 | 20 65 78 61 6d 70 6c 65 |hout the| example|
|00000e90| 2e 29 0a 54 68 65 20 61 | 62 73 74 72 61 63 74 69 |.).The a|bstracti|
|00000ea0| 6f 6e 20 66 75 6e 63 74 | 69 6f 6e 20 77 6f 72 6b |on funct|ion work|
|00000eb0| 73 20 62 79 20 70 65 65 | 6c 69 6e 67 20 6f 66 66 |s by pee|ling off|
|00000ec0| 20 74 68 65 20 74 6f 70 | 20 65 6c 65 6d 65 6e 74 | the top| element|
|00000ed0| 2c 20 61 6e 64 0a 70 75 | 73 68 69 6e 67 20 69 74 |, and.pu|shing it|
|00000ee0| 20 6f 6e 74 6f 20 74 68 | 65 20 61 62 73 74 72 61 | onto th|e abstra|
|00000ef0| 63 74 69 6f 6e 20 6f 66 | 20 77 68 61 74 27 73 20 |ction of| what's |
|00000f00| 6c 65 66 74 2e 0a 54 68 | 69 73 20 77 6f 72 6b 73 |left..Th|is works|
|00000f10| 20 61 6c 6c 20 74 68 65 | 20 77 61 79 20 64 6f 77 | all the| way dow|
|00000f20| 6e 20 74 6f 20 7c 73 2e | 6c 3d 30 7c 2c 20 66 6f |n to |s.|l=0|, fo|
|00000f30| 72 20 77 68 69 63 68 20 | 74 68 65 20 61 62 73 74 |r which |the abst|
|00000f40| 72 61 63 74 69 6f 6e 20 | 69 73 0a 7c 6e 65 77 5f |raction |is.|new_|
|00000f50| 73 74 61 63 6b 7c 2e 0a | 0a 54 68 65 20 74 65 6d |stack|..|.The tem|
|00000f60| 70 6c 61 74 65 73 20 66 | 6f 72 20 7c 69 6e 76 61 |plates f|or |inva|
|00000f70| 72 7c 20 61 6e 64 20 7c | 61 62 73 74 72 61 63 74 |r| and ||abstract|
|00000f80| 69 6f 6e 7c 20 61 72 65 | 20 67 65 6e 65 72 61 74 |ion| are| generat|
|00000f90| 65 64 0a 61 75 74 6f 6d | 61 74 69 63 61 6c 6c 79 |ed.autom|atically|
|00000fa0| 2e 0a 0a 40 3c 41 62 73 | 74 72 61 63 74 69 6f 6e |...@<Abs|traction|
|00000fb0| 2e 2e 2e 40 3e 3d 0a 0a | 0a 0a 0a 0a 0a 0a 0a 0a |...@>=..|........|
|00000fc0| 0a 0a 0a 0a 0a 0a 0a 0a | 40 20 54 6f 20 69 6d 70 |........|@ To imp|
|00000fd0| 6c 65 6d 65 6e 74 20 7c | 65 6d 70 74 79 5f 73 74 |lement ||empty_st|
|00000fe0| 61 63 6b 7c 20 77 65 20 | 72 65 74 75 72 6e 20 61 |ack| we |return a|
|00000ff0| 20 73 74 61 63 6b 20 6f | 66 20 6c 65 6e 67 74 68 | stack o|f length|
|00001000| 20 7a 65 72 6f 2e 0a 0a | 40 3c 49 6d 70 6c 65 6d | zero...|@<Implem|
|00001010| 65 6e 74 61 74 69 6f 6e | 20 6f 66 20 7c 65 6d 70 |entation| of |emp|
|00001020| 74 79 5f 73 74 61 63 6b | 7c 40 3e 3d 0a 66 75 6e |ty_stack||@>=.fun|
|00001030| 63 74 69 6f 6e 20 65 6d | 70 74 79 5f 73 74 61 63 |ction em|pty_stac|
|00001040| 6b 20 72 65 74 75 72 6e | 20 73 74 61 63 6b 0a 0a |k return| stack..|
|00001050| 0a 0a 0a 0a 69 73 0a 09 | 65 6d 70 74 79 3a 20 73 |....is..|empty: s|
|00001060| 74 61 63 6b 3b 0a 62 65 | 67 69 6e 0a 09 65 6d 70 |tack;.be|gin..emp|
|00001070| 74 79 2e 6c 20 3a 3d 20 | 30 3b 0a 20 20 20 20 20 |ty.l := |0;. |
|00001080| 20 20 20 72 65 74 75 72 | 6e 20 65 6d 70 74 79 3b | retur|n empty;|
|00001090| 0a 65 6e 64 20 65 6d 70 | 74 79 5f 73 74 61 63 6b |.end emp|ty_stack|
|000010a0| 3b 0a 0a 40 2a 50 72 6f | 6f 66 20 6f 66 20 7c 65 |;..@*Pro|of of |e|
|000010b0| 6d 70 74 79 5f 73 74 61 | 63 6b 7c 2e 0a 48 65 72 |mpty_sta|ck|..Her|
|000010c0| 65 20 61 6e 64 20 65 6c | 73 65 77 68 65 72 65 20 |e and el|sewhere |
|000010d0| 77 65 20 77 69 6c 6c 20 | 75 73 65 20 74 68 65 20 |we will |use the |
|000010e0| 6e 6f 74 61 74 69 6f 6e | 20 7c 40 40 72 65 74 75 |notation| |@@retu|
|000010f0| 72 6e 7c 20 74 6f 20 64 | 65 6e 6f 74 65 20 74 68 |rn| to d|enote th|
|00001100| 65 20 72 65 74 75 72 6e | 0a 76 61 6c 75 65 2e 0a |e return|.value..|
|00001110| 50 72 65 64 69 63 61 74 | 65 20 74 72 61 6e 73 66 |Predicat|e transf|
|00001120| 6f 72 6d 61 74 69 6f 6e | 20 6f 66 20 74 68 65 20 |ormation| of the |
|00001130| 70 6f 73 74 63 6f 6e 64 | 69 74 69 6f 6e 20 6c 65 |postcond|ition le|
|00001140| 61 76 65 73 20 74 68 65 | 20 66 6f 6c 6c 6f 77 69 |aves the| followi|
|00001150| 6e 67 20 76 65 72 69 66 | 69 63 61 74 69 6f 6e 0a |ng verif|ication.|
|00001160| 63 6f 6e 64 69 74 69 6f | 6e 3a 0a 5c 56 43 7b 7c |conditio|n:.\VC{||
|00001170| 74 72 75 65 7c 7d 7b 7c | 69 6e 76 61 72 28 65 6d |true|}{||invar(em|
|00001180| 70 74 79 29 20 61 6e 64 | 20 61 62 73 74 72 61 63 |pty) and| abstrac|
|00001190| 74 69 6f 6e 28 65 6d 70 | 74 79 29 3d 6e 65 77 5f |tion(emp|ty)=new_|
|000011a0| 73 74 61 63 6b 7c 7d 0a | 0a 57 65 20 73 70 6c 69 |stack|}.|.We spli|
|000011b0| 74 20 61 6e 64 20 67 65 | 74 0a 5c 56 43 7b 7c 74 |t and ge|t.\VC{|t|
|000011c0| 72 75 65 7c 7d 7b 7c 69 | 6e 76 61 72 28 65 6d 70 |rue|}{|i|nvar(emp|
|000011d0| 74 79 29 7c 7d 0a 61 6e | 64 2c 20 65 78 70 61 6e |ty)|}.an|d, expan|
|000011e0| 64 69 6e 67 0a 5c 56 43 | 7b 7c 74 72 75 65 7c 7d |ding.\VC|{|true|}|
|000011f0| 7b 7c 30 3c 3d 65 6d 70 | 74 79 2e 6c 20 61 6e 64 |{|0<=emp|ty.l and|
|00001200| 20 65 6d 70 74 79 2e 6c | 20 3c 3d 20 6c 65 6e 67 | empty.l| <= leng|
|00001210| 74 68 7c 7d 0a 61 6e 64 | 20 73 75 62 73 74 69 74 |th|}.and| substit|
|00001220| 75 74 69 6e 67 20 66 6f | 72 20 7c 65 6d 70 74 79 |uting fo|r |empty|
|00001230| 2e 6c 7c 20 28 6f 6e 20 | 77 68 61 74 20 62 61 73 |.l| (on |what bas|
|00001240| 69 73 3f 29 0a 5c 56 43 | 7b 7c 74 72 75 65 7c 7d |is?).\VC|{|true|}|
|00001250| 7b 7c 30 3c 3d 30 20 61 | 6e 64 20 30 20 3c 3d 20 |{|0<=0 a|nd 0 <= |
|00001260| 6c 65 6e 67 74 68 7c 7d | 0a 66 72 6f 6d 20 77 68 |length|}|.from wh|
|00001270| 69 63 68 0a 5c 56 43 7b | 7c 74 72 75 65 7c 7d 7b |ich.\VC{||true|}{|
|00001280| 7c 74 72 75 65 7c 7d 0a | 62 65 63 61 75 73 65 20 ||true|}.|because |
|00001290| 6f 66 20 74 68 65 20 70 | 72 6f 70 65 72 74 79 20 |of the p|roperty |
|000012a0| 7c 30 3c 3d 6e 7c 20 66 | 6f 72 20 61 6e 79 20 6e ||0<=n| f|or any n|
|000012b0| 61 74 75 72 61 6c 20 6e | 75 6d 62 65 72 20 7c 6e |atural n|umber |n|
|000012c0| 7c 2e 0a 0a 54 68 65 20 | 73 65 63 6f 6e 64 20 76 ||...The |second v|
|000012d0| 65 72 69 66 69 63 61 74 | 69 6f 6e 20 63 6f 6e 64 |erificat|ion cond|
|000012e0| 69 74 69 6f 6e 20 69 73 | 0a 5c 56 43 7b 7c 74 72 |ition is|.\VC{|tr|
|000012f0| 75 65 7c 7d 7b 7c 61 62 | 73 74 72 61 63 74 69 6f |ue|}{|ab|stractio|
|00001300| 6e 28 65 6d 70 74 79 29 | 3d 6e 65 77 5f 73 74 61 |n(empty)|=new_sta|
|00001310| 63 6b 7c 7d 0a 57 65 20 | 65 78 70 61 6e 64 20 7c |ck|}.We |expand ||
|00001320| 61 62 73 74 72 61 63 74 | 69 6f 6e 7c 2c 20 73 70 |abstract|ion|, sp|
|00001330| 61 77 6e 69 6e 67 20 74 | 68 65 20 6e 65 77 20 56 |awning t|he new V|
|00001340| 43 0a 5c 56 43 7b 7c 74 | 72 75 65 7c 7d 7b 7c 69 |C.\VC{|t|rue|}{|i|
|00001350| 6e 76 61 72 28 65 6d 70 | 74 79 29 7c 7d 0a 66 6f |nvar(emp|ty)|}.fo|
|00001360| 72 20 77 68 69 63 68 20 | 77 65 20 63 61 6e 20 72 |r which |we can r|
|00001370| 65 66 65 72 20 74 6f 20 | 74 68 65 20 65 61 72 6c |efer to |the earl|
|00001380| 69 65 72 20 70 72 6f 6f | 66 2e 0a 57 65 20 61 72 |ier proo|f..We ar|
|00001390| 65 20 6c 65 66 74 20 77 | 69 74 68 0a 5c 56 43 7b |e left w|ith.\VC{|
|000013a0| 7c 74 72 75 65 7c 7d 7b | 7c 69 66 20 65 6d 70 74 ||true|}{||if empt|
|000013b0| 79 2e 6c 3d 30 20 74 68 | 65 6e 20 6e 65 77 5f 73 |y.l=0 th|en new_s|
|000013c0| 74 61 63 6b 20 65 6c 73 | 65 0a 20 20 20 20 20 20 |tack els|e. |
|000013d0| 20 20 20 70 75 73 68 28 | 61 62 73 74 72 61 63 74 | push(|abstract|
|000013e0| 69 6f 6e 28 65 6d 70 74 | 79 5b 6c 3d 3e 6c 2d 31 |ion(empt|y[l=>l-1|
|000013f0| 5d 29 2c 65 6d 70 74 79 | 2e 61 28 65 6d 70 74 79 |]),empty|.a(empty|
|00001400| 2e 6c 29 29 3b 0a 20 20 | 20 20 20 65 6e 64 20 69 |.l));. | end i|
|00001410| 66 20 3d 20 6e 65 77 5f | 73 74 61 63 6b 3b 7c 7d |f = new_|stack;|}|
|00001420| 0a 57 68 69 63 68 20 72 | 65 77 72 69 74 65 73 20 |.Which r|ewrites |
|00001430| 74 6f 0a 5c 56 43 7b 7c | 74 72 75 65 7c 7d 7b 7c |to.\VC{||true|}{||
|00001440| 6e 65 77 5f 73 74 61 63 | 6b 3d 6e 65 77 5f 73 74 |new_stac|k=new_st|
|00001450| 61 63 6b 7c 7d 0a 0a 0a | 40 20 48 65 72 65 20 77 |ack|}...|@ Here w|
|00001460| 65 20 68 61 76 65 20 74 | 6f 20 63 68 65 63 6b 20 |e have t|o check |
|00001470| 66 6f 72 20 6f 76 65 72 | 66 6c 6f 77 2c 20 62 75 |for over|flow, bu|
|00001480| 74 20 74 68 65 72 65 20 | 61 72 65 20 72 65 61 6c |t there |are real|
|00001490| 6c 79 20 6e 6f 20 73 75 | 72 70 72 69 73 65 73 2e |ly no su|rprises.|
|000014a0| 0a 40 3c 49 6d 70 6c 65 | 6d 65 6e 74 61 74 69 6f |.@<Imple|mentatio|
|000014b0| 6e 20 6f 66 20 7c 70 75 | 73 68 69 74 7c 40 3e 3d |n of |pu|shit|@>=|
|000014c0| 0a 66 75 6e 63 74 69 6f | 6e 20 70 75 73 68 69 74 |.functio|n pushit|
|000014d0| 28 73 3a 73 74 61 63 6b | 3b 20 65 3a 65 6c 65 6d |(s:stack|; e:elem|
|000014e0| 65 6e 74 29 20 72 65 74 | 75 72 6e 20 73 74 61 63 |ent) ret|urn stac|
|000014f0| 6b 0a 0a 0a 0a 0a 0a 0a | 69 73 0a 20 20 20 20 20 |k.......|is. |
|00001500| 20 20 20 74 3a 20 73 74 | 61 63 6b 3b 0a 62 65 67 | t: st|ack;.beg|
|00001510| 69 6e 0a 20 20 20 20 20 | 20 20 20 69 66 20 73 2e |in. | if s.|
|00001520| 6c 3d 6c 65 6e 67 74 68 | 20 74 68 65 6e 20 72 61 |l=length| then ra|
|00001530| 69 73 65 20 6f 76 65 72 | 66 6c 6f 77 3b 20 65 6e |ise over|flow; en|
|00001540| 64 20 69 66 3b 0a 20 20 | 20 20 20 20 20 20 74 2e |d if;. | t.|
|00001550| 6c 20 3a 3d 20 73 2e 6c | 2b 31 3b 0a 20 20 20 20 |l := s.l|+1;. |
|00001560| 20 20 20 20 74 2e 61 20 | 3a 3d 20 73 2e 61 3b 0a | t.a |:= s.a;.|
|00001570| 20 20 20 20 20 20 20 20 | 74 2e 61 28 74 2e 6c 29 | |t.a(t.l)|
|00001580| 20 3a 3d 20 65 3b 0a 20 | 20 20 20 20 20 20 20 72 | := e;. | r|
|00001590| 65 74 75 72 6e 20 74 3b | 0a 65 6e 64 20 65 6d 70 |eturn t;|.end emp|
|000015a0| 74 79 5f 73 74 61 63 6b | 3b 0a 0a 40 2a 50 72 65 |ty_stack|;..@*Pre|
|000015b0| 64 69 63 61 74 65 20 74 | 72 61 6e 73 66 6f 72 6d |dicate t|ransform|
|000015c0| 61 74 69 6f 6e 20 6f 66 | 20 7c 70 75 73 68 69 74 |ation of| |pushit|
|000015d0| 7c 2e 0a 48 65 72 65 20 | 77 65 20 68 61 76 65 20 ||..Here |we have |
|000015e0| 69 67 6e 6f 72 65 64 20 | 74 68 65 20 70 6f 73 73 |ignored |the poss|
|000015f0| 69 62 69 6c 69 74 79 20 | 6f 66 20 61 62 6e 6f 72 |ibility |of abnor|
|00001600| 6d 61 6c 20 74 65 72 6d | 69 6e 61 74 69 6f 6e 2e |mal term|ination.|
|00001610| 0a 0a 49 27 76 65 20 77 | 72 69 74 74 65 6e 20 69 |..I've w|ritten i|
|00001620| 6e 74 65 72 6d 65 64 69 | 61 74 65 20 63 6f 6e 64 |ntermedi|ate cond|
|00001630| 69 74 69 6f 6e 73 20 69 | 6e 20 62 65 74 77 65 65 |itions i|n betwee|
|00001640| 6e 20 74 68 65 20 73 74 | 61 74 65 6d 65 6e 74 73 |n the st|atements|
|00001650| 20 74 6f 0a 77 68 69 63 | 68 20 74 68 65 79 20 61 | to.whic|h they a|
|00001660| 70 70 6c 79 2e 0a 54 68 | 65 20 70 72 65 64 69 63 |pply..Th|e predic|
|00001670| 61 74 65 20 74 72 61 6e | 73 66 6f 72 6d 61 74 69 |ate tran|sformati|
|00001680| 6f 6e 20 72 75 6c 65 73 | 20 49 27 76 65 20 75 73 |on rules| I've us|
|00001690| 65 64 20 61 72 65 20 63 | 6f 6d 70 6c 65 74 65 6c |ed are c|ompletel|
|000016a0| 79 0a 69 6e 66 6f 72 6d | 61 6c 2e 0a 0a 0a 40 63 |y.inform|al....@c|
|000016b0| 0a 66 75 6e 63 74 69 6f | 6e 20 70 75 73 68 69 74 |.functio|n pushit|
|000016c0| 28 73 3a 73 74 61 63 6b | 3b 20 65 3a 65 6c 65 6d |(s:stack|; e:elem|
|000016d0| 65 6e 74 29 20 72 65 74 | 75 72 6e 20 73 74 61 63 |ent) ret|urn stac|
|000016e0| 6b 0a 0a 0a 0a 0a 0a 0a | 0a 69 73 0a 20 20 20 20 |k.......|.is. |
|000016f0| 20 20 20 20 74 3a 20 73 | 74 61 63 6b 3b 0a 62 65 | t: s|tack;.be|
|00001700| 67 69 6e 0a 0a 0a 0a 20 | 20 20 20 20 20 20 20 69 |gin.... | i|
|00001710| 66 20 73 2e 6c 3d 6c 65 | 6e 67 74 68 20 74 68 65 |f s.l=le|ngth the|
|00001720| 6e 20 72 61 69 73 65 20 | 6f 76 65 72 66 6c 6f 77 |n raise |overflow|
|00001730| 3b 20 65 6e 64 20 69 66 | 3b 0a 0a 0a 20 20 20 20 |; end if|;... |
|00001740| 20 20 20 20 74 2e 6c 20 | 3a 3d 20 73 2e 6c 2b 31 | t.l |:= s.l+1|
|00001750| 3b 0a 0a 0a 20 20 20 20 | 20 20 20 20 74 2e 61 20 |;... | t.a |
|00001760| 3a 3d 20 73 2e 61 3b 0a | 0a 0a 20 20 20 20 20 20 |:= s.a;.|.. |
|00001770| 20 20 74 2e 61 28 74 2e | 6c 29 20 3a 3d 20 65 3b | t.a(t.|l) := e;|
|00001780| 0a 0a 0a 20 20 20 20 20 | 20 20 20 72 65 74 75 72 |... | retur|
|00001790| 6e 20 74 3b 0a 0a 0a 65 | 6e 64 20 65 6d 70 74 79 |n t;...e|nd empty|
|000017a0| 5f 73 74 61 63 6b 3b 0a | 0a 40 2a 50 72 6f 6f 66 |_stack;.|.@*Proof|
|000017b0| 20 6f 66 20 7c 70 75 73 | 68 69 74 7c 2e 0a 57 65 | of |pus|hit|..We|
|000017c0| 27 72 65 20 67 6f 69 6e | 67 20 74 6f 20 6d 61 6b |'re goin|g to mak|
|000017d0| 65 20 68 65 61 76 79 20 | 75 73 65 20 6f 66 20 61 |e heavy |use of a|
|000017e0| 20 28 6e 6f 6e 65 78 69 | 73 74 65 6e 74 29 20 74 | (nonexi|stent) t|
|000017f0| 68 65 6f 72 79 20 6f 66 | 20 72 65 63 6f 72 64 73 |heory of| records|
|00001800| 2e 0a 52 65 63 6f 72 64 | 20 73 74 61 74 65 73 20 |..Record| states |
|00001810| 61 72 65 20 61 73 20 69 | 6e 20 41 6e 6e 61 3b 0a |are as i|n Anna;.|
|00001820| 69 6e 66 6f 72 6d 61 6c | 6c 79 20 74 68 65 79 20 |informal|ly they |
|00001830| 62 65 68 61 76 65 20 6a | 75 73 74 20 61 73 20 79 |behave j|ust as y|
|00001840| 6f 75 20 77 6f 75 6c 64 | 20 74 68 69 6e 6b 2e 0a |ou would| think..|
|00001850| 0a 57 65 20 66 69 72 73 | 74 20 72 65 77 72 69 74 |.We firs|t rewrit|
|00001860| 65 20 74 68 65 20 74 65 | 72 6d 20 69 6e 76 6f 6c |e the te|rm invol|
|00001870| 76 69 6e 67 20 7c 74 7c | 20 69 6e 74 6f 20 61 20 |ving |t|| into a |
|00001880| 73 69 6d 70 6c 65 72 20 | 61 6e 64 20 6d 6f 72 65 |simpler |and more|
|00001890| 20 75 73 65 66 75 6c 0a | 66 6f 72 6d 3a 0a 24 24 | useful.|form:.$$|
|000018a0| 5c 76 62 6f 78 7b 5c 6e | 6f 69 6e 64 65 6e 74 0a |\vbox{\n|oindent.|
|000018b0| 7c 74 5b 6c 3d 3e 73 2e | 6c 2b 31 3b 61 3d 3e 73 ||t[l=>s.|l+1;a=>s|
|000018c0| 2e 61 3b 61 28 6c 29 3d | 3e 65 5d 7c 20 72 65 77 |.a;a(l)=|>e]| rew|
|000018d0| 72 69 74 65 73 20 74 6f | 0a 7c 73 5b 6c 3d 3e 6c |rites to|.|s[l=>l|
|000018e0| 2b 31 3b 61 28 6c 29 3d | 3e 65 5d 7c 2e 0a 7d 24 |+1;a(l)=|>e]|..}$|
|000018f0| 24 0a 0a 0a 41 66 74 65 | 72 20 74 68 69 73 20 73 |$...Afte|r this s|
|00001900| 69 6d 70 6c 69 66 69 63 | 61 74 69 6f 6e 20 77 65 |implific|ation we|
|00001910| 20 68 61 76 65 20 74 68 | 69 73 20 76 65 72 69 66 | have th|is verif|
|00001920| 69 63 61 74 69 6f 6e 20 | 63 6f 6e 64 69 74 69 6f |ication |conditio|
|00001930| 6e 3a 0a 5c 56 43 7b 7c | 0a 69 6e 76 61 72 28 73 |n:.\VC{||.invar(s|
|00001940| 29 7c 5c 69 74 65 6d 20 | 0a 7c 6e 6f 74 20 28 73 |)|\item |.|not (s|
|00001950| 69 7a 65 28 61 62 73 74 | 72 61 63 74 69 6f 6e 28 |ize(abst|raction(|
|00001960| 73 29 29 20 3d 20 6c 65 | 6e 67 74 68 29 7c 7d 0a |s)) = le|ngth)|}.|
|00001970| 7b 7c 0a 73 2e 6c 20 2f | 3d 20 6c 65 6e 67 74 68 |{|.s.l /|= length|
|00001980| 20 61 6e 64 0a 69 6e 76 | 61 72 28 73 5b 6c 3d 3e | and.inv|ar(s[l=>|
|00001990| 6c 2b 31 3b 61 28 6c 29 | 3d 3e 65 5d 29 20 61 6e |l+1;a(l)|=>e]) an|
|000019a0| 64 0a 61 62 73 74 72 61 | 63 74 69 6f 6e 28 73 5b |d.abstra|ction(s[|
|000019b0| 6c 3d 3e 6c 2b 31 3b 61 | 28 6c 29 3d 3e 65 5d 29 |l=>l+1;a|(l)=>e])|
|000019c0| 3d 70 75 73 68 28 61 62 | 73 74 72 61 63 74 69 6f |=push(ab|stractio|
|000019d0| 6e 28 73 29 2c 65 29 0a | 7c 7d 0a 57 65 27 6c 6c |n(s),e).||}.We'll|
|000019e0| 20 74 61 63 6b 6c 65 20 | 6f 6e 65 20 63 6f 6e 6a | tackle |one conj|
|000019f0| 75 6e 63 74 20 61 74 20 | 61 20 74 69 6d 65 2e 0a |unct at |a time..|
|00001a00| 0a 40 20 7b 5c 69 74 20 | 46 69 72 73 74 20 63 6f |.@ {\it |First co|
|00001a10| 6e 6a 75 6e 63 74 2e 7d | 0a 57 65 20 62 65 67 69 |njunct.}|.We begi|
|00001a20| 6e 20 62 79 20 70 72 6f | 76 69 6e 67 20 61 20 6c |n by pro|ving a l|
|00001a30| 65 6d 6d 61 20 61 62 6f | 75 74 20 7c 73 69 7a 65 |emma abo|ut |size|
|00001a40| 7c 3a 0a 5c 56 43 7b 7c | 69 6e 76 61 72 28 73 29 ||:.\VC{||invar(s)|
|00001a50| 7c 7d 0a 7b 7c 73 69 7a | 65 28 61 62 73 74 72 61 ||}.{|siz|e(abstra|
|00001a60| 63 74 69 6f 6e 28 73 29 | 29 7c 24 5c 73 69 6d 65 |ction(s)|)|$\sime|
|00001a70| 71 24 7c 73 2e 6c 7c 7d | 0a 54 68 65 20 70 72 6f |q$|s.l|}|.The pro|
|00001a80| 6f 66 20 69 73 20 62 79 | 20 74 79 70 65 20 69 6e |of is by| type in|
|00001a90| 64 75 63 74 69 6f 6e 20 | 6f 6e 20 74 68 65 20 70 |duction |on the p|
|00001aa0| 72 65 64 65 66 69 6e 65 | 64 20 74 79 70 65 20 7c |redefine|d type ||
|00001ab0| 6e 61 74 75 72 61 6c 7c | 2e 0a 57 65 20 6f 6d 69 |natural||..We omi|
|00001ac0| 74 20 69 74 20 68 65 72 | 65 2e 0a 0a 4f 6e 63 65 |t it her|e...Once|
|00001ad0| 20 77 65 20 68 61 76 65 | 20 74 68 65 20 7c 73 69 | we have| the |si|
|00001ae0| 7a 65 7c 20 6c 65 6d 6d | 61 20 77 65 20 72 65 77 |ze| lemm|a we rew|
|00001af0| 72 69 74 65 20 74 68 65 | 20 56 43 20 66 6f 72 20 |rite the| VC for |
|00001b00| 74 68 65 20 66 69 72 73 | 74 20 63 6f 6e 6a 75 6e |the firs|t conjun|
|00001b10| 63 74 20 61 73 3a 0a 5c | 56 43 7b 7c 0a 69 6e 76 |ct as:.\|VC{|.inv|
|00001b20| 61 72 28 73 29 7c 5c 69 | 74 65 6d 20 0a 7c 6e 6f |ar(s)|\i|tem .|no|
|00001b30| 74 20 28 73 2e 6c 20 3d | 20 6c 65 6e 67 74 68 29 |t (s.l =| length)|
|00001b40| 7c 7d 0a 7b 7c 73 2e 6c | 20 2f 3d 20 6c 65 6e 67 ||}.{|s.l| /= leng|
|00001b50| 74 68 7c 7d 0a 54 68 65 | 20 70 72 6f 6f 66 20 69 |th|}.The| proof i|
|00001b60| 73 20 62 79 20 74 68 65 | 20 6c 61 77 73 20 28 6e |s by the| laws (n|
|00001b70| 6f 74 20 73 74 61 74 65 | 64 29 20 66 6f 72 20 7c |ot state|d) for ||
|00001b80| 3d 7c 20 61 6e 64 20 7c | 2f 3d 7c 2e 0a 0a 40 20 |=| and ||/=|...@ |
|00001b90| 7b 5c 69 74 20 53 65 63 | 6f 6e 64 20 43 6f 6e 6a |{\it Sec|ond Conj|
|00001ba0| 75 6e 63 74 2e 7d 0a 41 | 67 61 69 6e 20 77 65 20 |unct.}.A|gain we |
|00001bb0| 61 70 70 6c 79 20 74 68 | 65 20 7c 73 69 7a 65 7c |apply th|e |size||
|00001bc0| 20 6c 65 6d 6d 61 2e 0a | 5c 56 43 7b 7c 0a 69 6e | lemma..|\VC{|.in|
|00001bd0| 76 61 72 28 73 29 7c 5c | 69 74 65 6d 20 0a 7c 6e |var(s)|\|item .|n|
|00001be0| 6f 74 20 28 73 2e 6c 20 | 3d 20 6c 65 6e 67 74 68 |ot (s.l |= length|
|00001bf0| 29 7c 7d 0a 7b 7c 0a 69 | 6e 76 61 72 28 73 5b 6c |)|}.{|.i|nvar(s[l|
|00001c00| 3d 3e 6c 2b 31 3b 61 28 | 6c 29 3d 3e 65 5d 29 7c |=>l+1;a(|l)=>e])||
|00001c10| 7d 0a 45 78 70 61 6e 64 | 69 6e 67 20 74 68 65 20 |}.Expand|ing the |
|00001c20| 64 65 66 69 6e 69 74 69 | 6f 6e 20 6f 66 20 7c 69 |definiti|on of |i|
|00001c30| 6e 76 61 72 7c 20 69 6e | 20 74 68 65 20 68 79 70 |nvar| in| the hyp|
|00001c40| 6f 74 68 65 73 69 73 20 | 61 6e 64 20 74 68 65 20 |othesis |and the |
|00001c50| 63 6f 6e 63 6c 75 73 69 | 6f 6e 20 79 69 65 6c 64 |conclusi|on yield|
|00001c60| 73 0a 5c 56 43 7b 7c 0a | 30 3c 3d 73 2e 6c 20 61 |s.\VC{|.|0<=s.l a|
|00001c70| 6e 64 20 73 2e 6c 20 3c | 3d 20 6c 65 6e 67 74 68 |nd s.l <|= length|
|00001c80| 7c 5c 69 74 65 6d 20 0a | 7c 6e 6f 74 20 28 73 2e ||\item .||not (s.|
|00001c90| 6c 20 3d 20 6c 65 6e 67 | 74 68 29 7c 7d 0a 7b 7c |l = leng|th)|}.{||
|00001ca0| 0a 30 3c 3d 73 5b 6c 3d | 3e 6c 2b 31 3b 61 28 6c |.0<=s[l=|>l+1;a(l|
|00001cb0| 29 3d 3e 65 5d 2e 6c 20 | 61 6e 64 0a 73 5b 6c 3d |)=>e].l |and.s[l=|
|00001cc0| 3e 6c 2b 31 3b 61 28 6c | 29 3d 3e 65 5d 2e 6c 3c |>l+1;a(l|)=>e].l<|
|00001cd0| 3d 6c 65 6e 67 74 68 0a | 7c 7d 0a 61 6e 64 20 77 |=length.||}.and w|
|00001ce0| 65 20 61 67 61 69 6e 20 | 65 78 70 6c 6f 69 74 20 |e again |exploit |
|00001cf0| 74 68 65 20 74 68 65 6f | 72 79 20 6f 66 20 72 65 |the theo|ry of re|
|00001d00| 63 6f 72 64 73 20 74 6f | 20 72 65 77 72 69 74 65 |cords to| rewrite|
|00001d10| 20 61 73 0a 5c 56 43 7b | 7c 0a 30 3c 3d 73 2e 6c | as.\VC{||.0<=s.l|
|00001d20| 20 61 6e 64 20 73 2e 6c | 20 3c 3d 20 6c 65 6e 67 | and s.l| <= leng|
|00001d30| 74 68 7c 5c 69 74 65 6d | 20 0a 7c 6e 6f 74 20 28 |th|\item| .|not (|
|00001d40| 73 2e 6c 20 3d 20 6c 65 | 6e 67 74 68 29 7c 7d 0a |s.l = le|ngth)|}.|
|00001d50| 7b 7c 0a 30 3c 3d 73 2e | 6c 2b 31 20 61 6e 64 0a |{|.0<=s.|l+1 and.|
|00001d60| 73 2e 6c 2b 31 3c 3d 6c | 65 6e 67 74 68 0a 7c 7d |s.l+1<=l|ength.|}|
|00001d70| 0a 41 6e 64 20 74 68 65 | 20 70 72 6f 6f 66 20 66 |.And the| proof f|
|00001d80| 6f 6c 6c 6f 77 73 20 62 | 79 20 7c 61 6e 64 7c 2d |ollows b|y |and|-|
|00001d90| 73 70 6c 69 74 74 69 6e | 67 20 68 79 70 6f 74 68 |splittin|g hypoth|
|00001da0| 65 73 65 73 20 61 6e 64 | 20 63 6f 6e 63 6c 75 73 |eses and| conclus|
|00001db0| 69 6f 6e 20 61 6e 64 20 | 62 79 0a 61 70 70 6c 79 |ion and |by.apply|
|00001dc0| 69 6e 67 20 74 68 65 20 | 6c 61 77 73 20 6f 66 20 |ing the |laws of |
|00001dd0| 61 72 69 74 68 6d 65 74 | 69 63 2e 0a 0a 40 20 7b |arithmet|ic...@ {|
|00001de0| 5c 69 74 20 54 68 69 72 | 64 20 63 6f 6e 6a 75 6e |\it Thir|d conjun|
|00001df0| 63 74 2e 7d 0a 54 68 69 | 73 20 69 73 20 74 68 65 |ct.}.Thi|s is the|
|00001e00| 20 69 6e 74 65 72 65 73 | 74 69 6e 67 20 70 61 72 | interes|ting par|
|00001e10| 74 2e 0a 57 65 20 65 78 | 70 61 6e 64 20 74 68 65 |t..We ex|pand the|
|00001e20| 20 64 65 66 69 6e 69 74 | 69 6f 6e 20 6f 66 20 7c | definit|ion of ||
|00001e30| 61 62 73 74 72 61 63 74 | 69 6f 6e 7c 20 6f 6e 20 |abstract|ion| on |
|00001e40| 74 68 65 20 6c 65 66 74 | 20 68 61 6e 64 20 73 69 |the left| hand si|
|00001e50| 64 65 20 6f 66 20 74 68 | 65 0a 63 6f 6e 63 6c 75 |de of th|e.conclu|
|00001e60| 73 69 6f 6e 2e 0a 54 68 | 69 73 20 73 70 61 77 6e |sion..Th|is spawn|
|00001e70| 73 20 61 20 56 43 20 73 | 68 6f 77 69 6e 67 20 74 |s a VC s|howing t|
|00001e80| 68 61 74 20 74 68 65 20 | 61 72 67 75 6d 65 6e 74 |hat the |argument|
|00001e90| 20 74 6f 20 7c 61 62 73 | 74 72 61 63 74 69 6f 6e | to |abs|traction|
|00001ea0| 7c 20 73 61 74 69 73 66 | 69 65 73 0a 7c 69 6e 76 || satisf|ies.|inv|
|00001eb0| 61 72 69 61 6e 74 7c 2c | 20 62 75 74 20 77 65 20 |ariant|,| but we |
|00001ec0| 64 69 64 20 74 68 61 74 | 20 65 61 72 6c 69 65 72 |did that| earlier|
|00001ed0| 2e 0a 0a 5c 56 43 7b 7c | 0a 69 6e 76 61 72 28 73 |...\VC{||.invar(s|
|00001ee0| 29 7c 5c 69 74 65 6d 20 | 0a 7c 6e 6f 74 20 28 73 |)|\item |.|not (s|
|00001ef0| 69 7a 65 28 61 62 73 74 | 72 61 63 74 69 6f 6e 28 |ize(abst|raction(|
|00001f00| 73 29 29 20 3d 20 6c 65 | 6e 67 74 68 29 7c 7d 0a |s)) = le|ngth)|}.|
|00001f10| 7b 7c 0a 69 66 20 73 5b | 6c 3d 3e 6c 2b 31 3b 61 |{|.if s[|l=>l+1;a|
|00001f20| 28 6c 29 3d 3e 65 5d 2e | 6c 3d 30 20 74 68 65 6e |(l)=>e].|l=0 then|
|00001f30| 20 6e 65 77 5f 73 74 61 | 63 6b 20 65 6c 73 65 0a | new_sta|ck else.|
|00001f40| 70 75 73 68 28 61 62 73 | 74 72 61 63 74 69 6f 6e |push(abs|traction|
|00001f50| 28 73 5b 6c 3d 3e 6c 2b | 31 3b 61 28 6c 29 3d 3e |(s[l=>l+|1;a(l)=>|
|00001f60| 65 3b 6c 3d 3e 6c 2d 31 | 5d 29 2c 0a 73 5b 6c 3d |e;l=>l-1|]),.s[l=|
|00001f70| 3e 6c 2b 31 3b 61 28 6c | 29 3d 3e 65 5d 2e 61 28 |>l+1;a(l|)=>e].a(|
|00001f80| 73 5b 6c 3d 3e 6c 2b 31 | 3b 61 28 6c 29 3d 3e 65 |s[l=>l+1|;a(l)=>e|
|00001f90| 5d 2e 6c 29 29 20 65 6e | 64 20 69 66 0a 20 3d 70 |].l)) en|d if. =p|
|00001fa0| 75 73 68 28 61 62 73 74 | 72 61 63 74 69 6f 6e 28 |ush(abst|raction(|
|00001fb0| 73 29 2c 65 29 0a 7c 7d | 0a 61 6e 64 2c 20 72 65 |s),e).|}|.and, re|
|00001fc0| 77 72 69 74 69 6e 67 20 | 61 63 63 6f 72 64 69 6e |writing |accordin|
|00001fd0| 67 20 74 6f 20 74 68 65 | 20 74 68 65 6f 72 79 20 |g to the| theory |
|00001fe0| 6f 66 20 72 65 63 6f 72 | 64 73 0a 28 65 73 70 65 |of recor|ds.(espe|
|00001ff0| 63 69 61 6c 6c 79 0a 7c | 73 5b 6c 3d 3e 6c 2b 31 |cially.||s[l=>l+1|
|00002000| 3b 61 28 6c 29 3d 3e 65 | 5d 2e 61 28 73 5b 6c 3d |;a(l)=>e|].a(s[l=|
|00002010| 3e 6c 2b 31 3b 61 28 6c | 29 3d 3e 65 5d 2e 6c 29 |>l+1;a(l|)=>e].l)|
|00002020| 7c 0a 72 65 77 72 69 74 | 65 73 20 74 6f 0a 7c 73 ||.rewrit|es to.|s|
|00002030| 5b 6c 3d 3e 6c 2b 31 3b | 61 28 73 2e 6c 2b 31 29 |[l=>l+1;|a(s.l+1)|
|00002040| 3d 3e 65 5d 2e 61 28 73 | 2e 6c 2b 31 29 7c 0a 77 |=>e].a(s|.l+1)|.w|
|00002050| 68 69 63 68 20 72 65 77 | 72 69 74 65 73 20 74 6f |hich rew|rites to|
|00002060| 20 7c 65 7c 29 3a 0a 5c | 56 43 7b 7c 0a 69 6e 76 | |e|):.\|VC{|.inv|
|00002070| 61 72 28 73 29 7c 5c 69 | 74 65 6d 20 0a 7c 6e 6f |ar(s)|\i|tem .|no|
|00002080| 74 20 28 73 69 7a 65 28 | 61 62 73 74 72 61 63 74 |t (size(|abstract|
|00002090| 69 6f 6e 28 73 29 29 20 | 3d 20 6c 65 6e 67 74 68 |ion(s)) |= length|
|000020a0| 29 7c 7d 0a 7b 7c 0a 69 | 66 20 73 2e 6c 2b 31 3d |)|}.{|.i|f s.l+1=|
|000020b0| 30 20 74 68 65 6e 20 6e | 65 77 5f 73 74 61 63 6b |0 then n|ew_stack|
|000020c0| 20 65 6c 73 65 0a 70 75 | 73 68 28 61 62 73 74 72 | else.pu|sh(abstr|
|000020d0| 61 63 74 69 6f 6e 28 73 | 5b 61 28 6c 2b 31 29 3d |action(s|[a(l+1)=|
|000020e0| 3e 65 5d 29 2c 65 29 20 | 65 6e 64 20 69 66 0a 20 |>e]),e) |end if. |
|000020f0| 3d 70 75 73 68 28 61 62 | 73 74 72 61 63 74 69 6f |=push(ab|stractio|
|00002100| 6e 28 73 29 2c 65 29 0a | 7c 7d 0a 41 70 70 6c 79 |n(s),e).||}.Apply|
|00002110| 69 6e 67 20 74 68 65 20 | 6c 61 77 73 20 6f 66 20 |ing the |laws of |
|00002120| 6e 61 74 75 72 61 6c 20 | 6e 75 6d 62 65 72 73 20 |natural |numbers |
|00002130| 77 65 20 68 61 76 65 0a | 5c 56 43 7b 7c 0a 69 6e |we have.|\VC{|.in|
|00002140| 76 61 72 28 73 29 7c 5c | 69 74 65 6d 20 0a 7c 6e |var(s)|\|item .|n|
|00002150| 6f 74 20 28 73 69 7a 65 | 28 61 62 73 74 72 61 63 |ot (size|(abstrac|
|00002160| 74 69 6f 6e 28 73 29 29 | 20 3d 20 6c 65 6e 67 74 |tion(s))| = lengt|
|00002170| 68 29 7c 7d 0a 7b 7c 0a | 70 75 73 68 28 61 62 73 |h)|}.{|.|push(abs|
|00002180| 74 72 61 63 74 69 6f 6e | 28 73 5b 61 28 6c 2b 31 |traction|(s[a(l+1|
|00002190| 29 3d 3e 65 5d 29 2c 65 | 29 20 3d 20 70 75 73 68 |)=>e]),e|) = push|
|000021a0| 28 61 62 73 74 72 61 63 | 74 69 6f 6e 28 73 29 2c |(abstrac|tion(s),|
|000021b0| 65 29 0a 7c 7d 0a 0a 0a | 41 6e 64 20 6e 6f 77 20 |e).|}...|And now |
|000021c0| 77 65 20 73 68 6f 77 20 | 62 79 20 61 20 6c 65 6d |we show |by a lem|
|000021d0| 6d 61 20 74 68 61 74 0a | 5c 56 43 7b 7c 69 6e 76 |ma that.|\VC{|inv|
|000021e0| 61 72 28 73 29 7c 5c 69 | 74 65 6d 20 7c 73 2e 6c |ar(s)|\i|tem |s.l|
|000021f0| 2f 3d 6c 65 6e 67 74 68 | 7c 7d 0a 7b 0a 7c 61 62 |/=length||}.{.|ab|
|00002200| 73 74 72 61 63 74 69 6f | 6e 28 73 5b 61 28 6c 2b |stractio|n(s[a(l+|
|00002210| 31 29 3d 3e 65 5d 29 7c | 24 5c 73 69 6d 65 71 24 |1)=>e])||$\simeq$|
|00002220| 7c 61 62 73 74 72 61 63 | 74 69 6f 6e 28 73 29 7c ||abstrac|tion(s)||
|00002230| 0a 7d 0a 77 68 69 63 68 | 20 69 73 20 73 75 66 66 |.}.which| is suff|
|00002240| 69 63 69 65 6e 74 2e 0a | 54 68 65 20 70 72 6f 6f |icient..|The proo|
|00002250| 66 20 6f 66 20 74 68 65 | 20 6c 65 6d 6d 61 20 69 |f of the| lemma i|
|00002260| 73 20 62 79 20 69 6e 64 | 75 63 74 69 6f 6e 20 6f |s by ind|uction o|
|00002270| 76 65 72 20 7c 6c 7c 20 | 28 74 79 70 65 20 69 6e |ver |l| |(type in|
|00002280| 64 75 63 74 69 6f 6e 20 | 6f 66 20 74 68 65 0a 70 |duction |of the.p|
|00002290| 72 65 64 65 66 69 6e 65 | 64 20 74 79 70 65 20 7c |redefine|d type ||
|000022a0| 6e 61 74 75 72 61 6c 7c | 29 2e 0a 0a 0a 0a 0a 40 |natural||)......@|
|000022b0| 20 40 3c 49 6d 70 6c 65 | 6d 65 6e 74 61 74 69 6f | @<Imple|mentatio|
|000022c0| 6e 20 6f 66 20 7c 70 6f | 70 69 74 7c 40 3e 3d 0a |n of |po|pit|@>=.|
|000022d0| 66 75 6e 63 74 69 6f 6e | 20 70 6f 70 69 74 28 73 |function| popit(s|
|000022e0| 3a 73 74 61 63 6b 29 20 | 72 65 74 75 72 6e 20 73 |:stack) |return s|
|000022f0| 74 61 63 6b 20 0a 0a 0a | 20 20 20 20 20 20 20 20 |tack ...| |
|00002300| 0a 09 0a 20 20 20 20 20 | 20 20 20 0a 0a 69 73 0a |... | ..is.|
|00002310| 09 74 3a 20 73 74 61 63 | 6b 3b 0a 62 65 67 69 6e |.t: stac|k;.begin|
|00002320| 0a 20 20 20 20 20 20 20 | 20 69 66 20 73 2e 6c 3d |. | if s.l=|
|00002330| 30 20 74 68 65 6e 20 72 | 61 69 73 65 20 75 6e 64 |0 then r|aise und|
|00002340| 65 72 66 6c 6f 77 3b 20 | 65 6e 64 20 69 66 3b 0a |erflow; |end if;.|
|00002350| 20 20 20 20 20 20 20 20 | 74 20 3a 3d 20 73 3b 0a | |t := s;.|
|00002360| 20 20 20 20 20 20 20 20 | 74 2e 6c 20 3a 3d 20 74 | |t.l := t|
|00002370| 2e 6c 2d 31 3b 0a 20 20 | 20 20 20 20 20 20 72 65 |.l-1;. | re|
|00002380| 74 75 72 6e 20 74 3b 0a | 65 6e 64 20 70 6f 70 69 |turn t;.|end popi|
|00002390| 74 3b 0a 0a 40 20 40 3c | 49 6d 70 6c 65 6d 65 6e |t;..@ @<|Implemen|
|000023a0| 74 61 74 69 6f 6e 20 6f | 66 20 7c 74 6f 70 69 74 |tation o|f |topit|
|000023b0| 7c 40 3e 3d 0a 66 75 6e | 63 74 69 6f 6e 20 74 6f ||@>=.fun|ction to|
|000023c0| 70 69 74 20 28 73 3a 73 | 74 61 63 6b 29 20 72 65 |pit (s:s|tack) re|
|000023d0| 74 75 72 6e 20 65 6c 65 | 6d 65 6e 74 20 0a 0a 0a |turn ele|ment ...|
|000023e0| 0a 0a 69 73 0a 62 65 67 | 69 6e 0a 20 20 20 20 20 |..is.beg|in. |
|000023f0| 20 20 20 69 66 20 73 2e | 6c 3d 30 20 74 68 65 6e | if s.|l=0 then|
|00002400| 20 72 61 69 73 65 20 75 | 6e 64 65 72 66 6c 6f 77 | raise u|nderflow|
|00002410| 3b 20 65 6e 64 20 69 66 | 3b 0a 20 20 20 20 20 20 |; end if|;. |
|00002420| 20 20 72 65 74 75 72 6e | 20 73 2e 61 28 73 2e 6c | return| s.a(s.l|
|00002430| 29 3b 0a 65 6e 64 20 74 | 6f 70 69 74 3b 0a 0a 40 |);.end t|opit;..@|
|00002440| 20 40 3c 49 6d 70 6c 65 | 6d 65 6e 74 61 74 69 6f | @<Imple|mentatio|
|00002450| 6e 20 6f 66 20 7c 69 73 | 45 6d 70 74 79 7c 40 3e |n of |is|Empty|@>|
|00002460| 3d 0a 20 20 20 20 66 75 | 6e 63 74 69 6f 6e 20 69 |=. fu|nction i|
|00002470| 73 45 6d 70 74 79 28 73 | 3a 73 74 61 63 6b 29 20 |sEmpty(s|:stack) |
|00002480| 72 65 74 75 72 6e 20 62 | 6f 6f 6c 65 61 6e 20 0a |return b|oolean .|
|00002490| 09 0a 09 0a 09 0a 09 0a | 09 69 73 0a 20 20 20 20 |........|.is. |
|000024a0| 62 65 67 69 6e 0a 09 72 | 65 74 75 72 6e 20 73 2e |begin..r|eturn s.|
|000024b0| 6c 3d 30 3b 0a 20 20 20 | 20 65 6e 64 20 69 73 45 |l=0;. | end isE|
|000024c0| 6d 70 74 79 3b 0a 40 20 | 50 72 65 64 69 63 61 74 |mpty;.@ |Predicat|
|000024d0| 65 20 74 72 61 6e 73 66 | 6f 72 6d 61 74 69 6f 6e |e transf|ormation|
|000024e0| 20 6f 66 20 69 73 45 6d | 70 74 79 2e 0a 40 63 0a | of isEm|pty..@c.|
|000024f0| 20 20 20 20 66 75 6e 63 | 74 69 6f 6e 20 69 73 45 | func|tion isE|
|00002500| 6d 70 74 79 28 73 3a 73 | 74 61 63 6b 29 20 72 65 |mpty(s:s|tack) re|
|00002510| 74 75 72 6e 20 62 6f 6f | 6c 65 61 6e 20 0a 09 0a |turn boo|lean ...|
|00002520| 09 0a 09 0a 09 0a 20 20 | 20 20 69 73 0a 20 20 20 |...... | is. |
|00002530| 20 62 65 67 69 6e 0a 09 | 0a 09 72 65 74 75 72 6e | begin..|..return|
|00002540| 20 73 2e 6c 3d 30 3b 0a | 09 0a 20 20 20 20 65 6e | s.l=0;.|.. en|
|00002550| 64 20 69 73 45 6d 70 74 | 79 3b 0a 0a 40 20 50 72 |d isEmpt|y;..@ Pr|
|00002560| 6f 6f 66 20 6f 66 20 69 | 73 45 6d 70 74 79 2e 0a |oof of i|sEmpty..|
|00002570| 5c 56 43 7b 7c 69 6e 76 | 61 72 69 61 6e 74 28 73 |\VC{|inv|ariant(s|
|00002580| 29 7c 7d 7b 7c 73 2e 6c | 3d 30 20 3d 69 73 5f 65 |)|}{|s.l|=0 =is_e|
|00002590| 6d 70 74 79 28 61 62 73 | 74 72 61 63 74 69 6f 6e |mpty(abs|traction|
|000025a0| 28 73 29 29 7c 7d 0a 45 | 78 70 61 6e 64 69 6e 67 |(s))|}.E|xpanding|
|000025b0| 20 7c 61 62 73 74 72 61 | 63 74 69 6f 6e 28 73 29 | |abstra|ction(s)|
|000025c0| 7c 2c 0a 5c 56 43 7b 7c | 69 6e 76 61 72 69 61 6e ||,.\VC{||invarian|
|000025d0| 74 28 73 29 7c 7d 7b 7c | 73 2e 6c 3d 30 20 3d 69 |t(s)|}{||s.l=0 =i|
|000025e0| 73 5f 65 6d 70 74 79 28 | 69 66 20 73 2e 6c 3d 30 |s_empty(|if s.l=0|
|000025f0| 20 74 68 65 6e 20 6e 69 | 6c 0a 09 09 65 6c 73 65 | then ni|l...else|
|00002600| 20 63 6f 6e 73 28 61 62 | 73 74 72 61 63 74 69 6f | cons(ab|stractio|
|00002610| 6e 28 73 5b 6c 3d 3e 6c | 2d 31 5d 29 2c 6c 2e 61 |n(s[l=>l|-1]),l.a|
|00002620| 28 73 2e 6c 2d 31 29 29 | 29 7c 7d 0a 53 69 6d 70 |(s.l-1))|)|}.Simp|
|00002630| 6c 69 66 79 69 6e 67 2c | 09 0a 5c 56 43 7b 7c 69 |lifying,|..\VC{|i|
|00002640| 6e 76 61 72 69 61 6e 74 | 28 73 29 7c 7d 7b 7c 28 |nvariant|(s)|}{|(|
|00002650| 73 2e 6c 3d 30 29 3d 69 | 66 20 73 2e 6c 3d 30 20 |s.l=0)=i|f s.l=0 |
|00002660| 74 68 65 6e 20 69 73 5f | 65 6d 70 74 79 28 6e 69 |then is_|empty(ni|
|00002670| 6c 29 0a 09 65 6c 73 65 | 20 69 73 5f 65 6d 70 74 |l)..else| is_empt|
|00002680| 79 28 63 6f 6e 73 28 61 | 62 73 74 72 61 63 74 69 |y(cons(a|bstracti|
|00002690| 6f 6e 28 73 5b 6c 3d 3e | 6c 2d 31 5d 29 2c 6c 2e |on(s[l=>|l-1]),l.|
|000026a0| 61 28 73 2e 6c 2d 31 29 | 29 29 7c 7d 0a 77 68 69 |a(s.l-1)|))|}.whi|
|000026b0| 63 68 20 77 65 20 63 61 | 6e 20 72 65 77 72 69 74 |ch we ca|n rewrit|
|000026c0| 65 20 61 73 0a 5c 56 43 | 7b 7c 69 6e 76 61 72 69 |e as.\VC|{|invari|
|000026d0| 61 6e 74 28 73 29 7c 7d | 7b 7c 28 73 2e 6c 3d 30 |ant(s)|}|{|(s.l=0|
|000026e0| 29 3d 69 66 20 73 2e 6c | 3d 30 20 74 68 65 6e 20 |)=if s.l|=0 then |
|000026f0| 74 72 75 65 0a 09 65 6c | 73 65 20 69 73 5f 65 6d |true..el|se is_em|
|00002700| 70 74 79 28 63 6f 6e 73 | 28 61 62 73 74 72 61 63 |pty(cons|(abstrac|
|00002710| 74 69 6f 6e 28 73 5b 6c | 3d 3e 6c 2d 31 5d 29 2c |tion(s[l|=>l-1]),|
|00002720| 6c 2e 61 28 73 2e 6c 2d | 31 29 29 29 7c 7d 0a 53 |l.a(s.l-|1)))|}.S|
|00002730| 69 6d 70 6c 69 66 79 69 | 6e 67 2c 0a 5c 56 43 7b |implifyi|ng,.\VC{|
|00002740| 7c 69 6e 76 61 72 69 61 | 6e 74 28 73 29 7c 7d 7b ||invaria|nt(s)|}{|
|00002750| 7c 74 72 75 65 7c 7d 0a | 0a 0a 40 2a 49 6e 64 65 ||true|}.|..@*Inde|
|00002760| 78 2e 0a 54 68 69 73 20 | 69 73 20 61 6e 20 69 6e |x..This |is an in|
|00002770| 64 65 78 20 6f 66 20 61 | 6c 6c 20 74 68 65 20 69 |dex of a|ll the i|
|00002780| 64 65 6e 74 69 66 69 65 | 72 73 20 75 73 65 64 20 |dentifie|rs used |
|00002790| 69 6e 20 74 68 65 20 70 | 72 6f 67 72 61 6d 2e 0a |in the p|rogram..|
|000027a0| 54 68 65 20 6e 75 6d 62 | 65 72 73 20 61 72 65 20 |The numb|ers are |
|000027b0| 73 65 63 74 69 6f 6e 20 | 6e 75 6d 62 65 72 73 2c |section |numbers,|
|000027c0| 20 6e 6f 74 20 70 61 67 | 65 20 6e 75 6d 62 65 72 | not pag|e number|
|000027d0| 73 2e | |s. | |
+--------+-------------------------+-------------------------+--------+--------+
